3 THE RANK THEOREM 279

Now consider K" as the product E1 x E2 with El = Kp, E2 = K*"*; we
are going to prove that the mapping (zl9 z2) -+fi(zl9 z2) =/(w~1(z1, z2)) of
F into F does not depend on z2, i.e. that D2/1(z1, z2) = 0 in F (8.6.1). By defini-
tion, we can write f(x) =/i /- H(f(x)\ I G(x)\9 hence by (8.9.2)

, 1

= D,/,

for any t e E. This yields

(10.3.11) D2/i H(/(x)), 1 G(x) • 0(0 = S, - #(/'(*) - 0

where Sx = rL,, - Dlt/i I - H(f(x))9 - <j(x) I is a linear mapping of Kp = E!

into F. We prove that Sx = 0 for any x e U0 . Indeed, if t e N, we have
G(/) = 0 by definition, hence Sx • H(f'(x) • t) = 0 by (10.3.1.1). But
/ -> H(f'(x) - 1) = ^'(^) • ^ is a bijection of N onto E! for x 6 U0 , and this
proves 5X = 0. From (10.3.1.1) we then deduce

for a/7^ r e E; but G maps E 0wfo E2 , hence by definition,

which is a linear mapping of E2 into F, is 0 for any x e U0 . The relation
D2/1(z1, z2) = 0 in I" then follows from the fact that

), I G(*))

is a homeomorphism of U0 onto an open set containing F.

We can now write fi(zi) instead of/1(z1,z2) and consider/! as a con-
tinuously differentiable mapping of El = Kp into F; we then have f(x) =

! (- H(f(x))\ for x e U; in other words, y =/i (- H(y)\ for y e/(U). This

roves that y-+- H(y) is a homeom
zi ~+fi(zi) ^e inverse homeomorphism.

proves that y-+- H(y) is a homeomorphism of /(U) onto lp c El9 andG(s) for any s e E, hence ^'(0) - c{ == et for